a, b:, E:({a..b}). (j:{a..b}. 0  E(j))  (i:{a..b}. E(i)  a  j < b. E(j)) 

latex

Definitions

ff, tt, if b then t else f fi , delta(i;j), T, P  Q, P  Q, {T}, SQType(T), True, P  Q, x. t(x), P & Q, , i  j < k, t  T, x(s), P  Q, {i..j}, x:A. B(x), Unit, , , S  T

Lemmas

qmul zero qrng, qmul one qrng, not functionality wrt iff, assert of bnot, assert of eq int, not wf, qle weakening eq qorder, eq int wf, or functionality wrt iff, assert of bor, bnot of lt int, bnot of le int, bnot thru band, true wf, squash wf, eqff to assert, assert of lt int, assert of le int, and functionality wrt iff, assert of band, eqtt to assert, iff transitivity, bool sq, bool cases, bnot wf, bor wf, qsum wf, delta wf, int-rational, qmul wf, qsum-qle, le wf, assert wf, bool wf, lt int wf, le int wf, band wf, rationals wf, int inc rationals, qle wf, int seg wf, qsum-delta